∧I INDUCTION;
∀E APPEND nil,v;
DISTRIB;
TAUTEQ nil=nil ;
TAUT (nil APP v)=v ↑↑↑:↑;
∃I ↑ v←w OCC ((2));
∀I ↑ v;
∀E APPEND u,v;
DISTRIB;
ASSUME ¬(u=nil);
TAUT (u APP v)=CONS(CAR u,CDR u APP v) ↑↑↑:↑;
ASSUME ∀v.∃w.(cdr u APP v)=w;
∀E ↑ v;
∃E ↑ w;
SUBSTR ↑ IN 11;
∀E CDR u;
SUBSTR ↑ IN ↑↑↑;
SUBSTR ↑ IN ↑↑↑;
∀E CAR u;
SUBST ↑ IN ↑↑;
∀E CONS car u,w;
SUBST ↑ IN ↑↑;
∃I ↑ cons(car u,w)←w;
∀I ↑ v;
⊃I 12⊃↑;
⊃I 10⊃↑;
TAUT (¬(u=nil)∧∀v.∃w.(cdr u APP v)=w)⊃∀v.∃w.(u APP v)=w ↑;
∀I ↑ u;
TAUT ∀u v.∃w.(u APP v)=w 1,7,↑;
∀E APPEND2 u,v;
DISTRIB;
∀E ↑↑↑ u,v;
TAUT (u app v)=(u APP v) ↑↑↑:↑;
∀I ↑ u v;
∀E ↑ cdr u,v;
∀E APPEND1 u,v;
∀E CDR u;
SUBSTR ↑ IN ↑↑↑ OCC 2;
SUBST ↑ IN ↑↑↑;
∀E CAR u;
SUBST ↑ IN ↑↑;
∀E CONS car u,cdr u app v;
SUBST ↑ IN ↑↑;
SUBST 33 IN ↑;
∀I ↑ u v;